Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		x * 1	→ x
2:		1 * y	→ y
3:		i(x) * x	→ 1
4:		x * i(x)	→ 1
5:		x * (y * z)	→ (x * y) * z
6:		i(1)	→ 1
7:		(x * y) * i(y)	→ x
8:		(x * i(y)) * y	→ x
9:		i(i(x))	→ x
10:		i(x * y)	→ i(y) * i(x)
11:		k(x,1)	→ 1
12:		k(x,x)	→ 1
13:		k(x,y) * k(y,x)	→ 1
14:		(i(x) * k(y,z)) * x	→ k((i(x) * y) * x,(i(x) * z) * x)
15:		k(x * i(y),y * i(x))	→ 1

There are 10 dependency pairs:


16:		x # (y z)	→ (x * y) *# z
17:		x # (y z)	→ x *# y
18:		I(x * y)	→ i(y) *# i(x)
19:		I(x * y)	→ I(y)
20:		I(x * y)	→ I(x)
21:		(i(x) * k(y,z)) *# x	→ K((i(x) * y) * x,(i(x) * z) * x)
22:		(i(x) * k(y,z)) *# x	→ (i(x) * y) *# x
23:		(i(x) * k(y,z)) *# x	→ i(x) *# y
24:		(i(x) * k(y,z)) *# x	→ (i(x) * z) *# x
25:		(i(x) * k(y,z)) *# x	→ i(x) *# z

The approximated dependency graph contains 2 SCCs: {16,17,22-25} and {19,20}.

Consider the SCC {16,17,22-25}. The constraints could not be solved.

Consider the SCC {19,20}. There are no usable rules. By taking the AF π with π(I) = 1 together with the lexicographic path order with empty precedence, the rules in {19,20} are strictly decreasing.

Tyrolean Termination Tool (0.11 seconds) --- May 4, 2006